Hoare 論理
Hoare logic
program$ Cが事前條件 (precondition)$ Pの下で實行され終了した時に事後條件 (postcondition)$ Qを滿たすなら$ \{P\}C\{Q\}と書く。これを Hoare triple と呼ぶ 公理
空文の公理$ \frac{}{\{P\}{\rm skip}\{P\}}
代入の公理$ \frac{}{\{P\lbrack E/x\rbrack\}x:=E\{P\}}
複合文の公理$ \frac{\{P\}S\{Q\}\quad\{Q\}T\{R\}}{\{P\}S;T\{R\}}
if の公理$ \frac{\{B\land P\}S\{Q\}\quad\{\neg B\land P\}T\{Q\}}{\{P\}{\rm if}~B~{\rm then}~S~{\rm else}~T~{\rm end}\{Q\}}
歸結の公理$ \frac{P_1\to P_2\quad\{P_2\}S\{Q_2\}\quad Q_2\to Q_1}{\{P_1\}S\{Q_1\}}
while の公理$ \frac{\{P\land B\}S\{P\}}{\{P\}{\rm while}~B~{\rm do}~S~{\rm done}\{\neg B\land P\}}
完全正當性の爲の while の公理。$ <_Dを集合$ D上の整礎關係とし、$ \frac{\{P\land B\land t=_D z\}S\{P\land t<_D z\}}{\{P\}{\rm while}~B~{\rm do}~S~{\rm done}\{\neg B\land P\}}
狀態變換子 (state transformer) / 述語變換子 (predicate transformer)
$ {\bf B}:=\{0,1\}
狀態變換子$ f:X\to Y,$ x_{\in X}\mapsto y_{\in Y}
述語變換子$ f^*:{\bf B}^Y\to{\bf B}^X,$ q_{:Y\to{\bf B}}\mapsto(f;q)_{:X\to{\bf B}}
述語變換意味論 (predicate transformer semantics)
$ Rを事後條件、$ Sを program とすると、最弱事前條件 (weakest precondition)$ {\rm wp}(S,R)が最低限滿たされてゐる必要が有る、とする
$ \{{\rm wp}(S,R)\}S\{R\}となる事前條件の內で最も弱いもの
述語變換子$ R\to{\rm wp}(S,R)が program$ Sの意味である
skip$ {\rm wp}({\rm skip},R)=R
abort$ {\rm wp}({\rm abort},R)=\bot
代入$ {\rm wp}(x:=E,R)=\forall y(y=E\implies E\lbrack x\larr y\rbrack)
順次處理$ {\rm wp}(S_1;S_2,R)={\rm wp}(S_1,{\rm wp}(S_2,R))
條件分岐$ {\rm wp}({\rm if}~E~{\rm then}~S_1{\rm else}~S_2~{\rm end},R)=(E\implies{\rm wp}(S_1,R))\land(\neg E\implies{\rm wp}(S_2,R))
while loop$ {\rm wlp}({\rm while}~E~{\rm do}~S~{\rm done},R)={\rm INV}~{\rm if}(E\land{\rm INV}\implies{\rm wlp}(S,{\rm INV}))\land(\neg E\land{\rm INV}\implies R)
完全正當性の爲の while loop$ {\rm wp}({\rm while}~E~{\rm do}~S~{\rm done},R)={\rm INV}~{\rm if}(E\land{\rm INV}\implies vf\in wfs)\land(E\land{\rm INV}\land v=vf\implies{\rm wp}(S,{\rm INV}\land v<vf))\land(\neg E\land{\rm INV}\implies R)
擴張
動的論理 (dynamic logic)$ P\to\lbrack C\rbrack Q